es:event_system{i:l}, i,x:Id, k:Knd. es-independent(es; i; k; x)  prop{i:l} 

latex

Definitions

t  T, x:A. B(x), es-V(es), f(a), x:AB(x), subtype(S; T), P  Q, False, A, A  B, , {x:A| B(x)} , , act(k), tag(k), lnk(k), isrcv(k), es-kindtype(es; i; k), locl(a), b, islocal(k), x:A  B(x), left + right, Knd, event_system{i:l}, Id, Unit, es-read-state(s), es-choose(es; i), Type, s = t, prop{i:l}, es-send(es; i), es-Msg(es), type List, es-trans(es; i), es-x-equiv(es; i; x; s1; s2), P  Q, es_state(es; i), es-independent(es; i; k; x)

Lemmas

es state wf, es-x-equiv wf, es-trans wf, es-Msg wf, es-send wf, assert wf, islocal wf, nat wf, es-choose wf, es-read-state wf, unit wf, es-kindtype wf, locl wf, actof wf, Knd wf, Id wf, event system wf, es-V wf